一階述語論理 (FOL)
first-order predicate logic (FOL)
命題論理 (殆どの場合は古典論理) に量化子$ \forall、$ \existを足したもの $ F\lbrack t/x\rbrackは、論理式$ Fでの變項$ xの全ての自由出現を、置き換へる事に依り新たに束縛される自由變項の無い (代入可能な (substitutable)) 別の項$ tに置き換へた論理式を表す
公理系
$ \forall x\phi\to\phi\lbrack t/x\rbrack普遍例化 (UI)
$ \forall x(\phi\to\psi)\to(\forall x\phi\to\forall x\psi)正規性
※$ tは任意の變項を表し、$ aは下式に現れない變項を表す事にする
論理規則
$ \forall(普遍汎化 (GEN)) :$ \frac{F\lbrack t/x\rbrack,\Gamma\vdash\Delta}{\forall xF,\Gamma\vdash\Delta}(\forall L),$ \frac{\Gamma\vdash\Delta,F\lbrack a/x\rbrack}{\Gamma\vdash\Delta,\forall xF}(\forall R)
$ \exist(存在汎化) :$ \frac{F\lbrack a/x\rbrack,\Gamma\vdash\Delta}{\exist xF,\Gamma\vdash\Delta}(\exist L),$ \frac{\Gamma\vdash\Delta,F\lbrack t/x\rbrack}{\Gamma\vdash\Delta,\exist xF}(\exist R)
汎化 / 例化
普遍汎化 (universal generalization。universal introduction。GEN)
$ \frac{\vdash F\lbrack t/x\rbrack}{\vdash\forall xF}論理式$ Fの自由變項$ xにどんな變項を代入してもよいなら$ xを全稱量化してよい
普遍例化 (universal instantiation。universal specification。universal elimination。UI)
$ \frac{\vdash\forall xF}{\vdash F\lbrack c/x\rbrack}論理式$ Fに現れる變項$ xを全稱量化してよいなら$ xに自由である定項を代入してよい
存在汎化 (existential generalization。existential introduction)
$ \frac{\vdash F\lbrack t/x\rbrack}{\vdash \exist xF}論理式$ Fの自由變項$ xにどんな變項を代入してもよいなら$ xを存在量化してよい
存在例化 (existential instantiation。existential elimination)
$ \frac{\vdash\exist xF}{\vdash F\lbrack c/x\rbrack}論理式$ Fに現れる變項$ xを存在量化してよいなら$ xに自由である定項を代入してよい
存在例化の誤謬
量化子 (限量子。quantifier)
全稱量化
存在量化
一意性$ \exist!
$ \exist!x.P(x)
$ \exist x(P(x)\land\forall y(P(x)\to x=y))
$ \exist x.P(x)\land\forall y,z((P(y)\land P(z))\to y=z)
$ \exist x\forall y(P(y)\lrarr x =y)
guard 附き量化
議論領域を指定する
量化子消去
擴張
動的述語論理 (dynamic predicate logic)
一般量化子